convert this float to a string with a fixed number of digits after the decimal point.
NYI: ENHANCEMENT: In the future, this should be replaced by a version of as_string with more formatting options,
as described here : https://github.com/tokiwa-software/fuzion/pull/7152#issuecomment-4613267795